| Definitions |  A, {T}, SQType(T),  x:A. B(x), P  Q, e' e.P(e'),  T,  e@i. P(e), A c B, pre-init1-p(es;i;x;X;x0;a;p;P), init-p-realizable, Rplus-right(x1), Rplus-left(x1), ff, Rplus?(x1),  b, True, Y, reduce(f;k;as),  (L), pre-p-realizable, es-realizer(p), t.2, t.1, P & Q, tt, if b then t else f fi , Top, s.x, preinit1R{$x:ut2, $a:ut2}(i; X; p; x0; P),   x. t(x),  , t  T, "$x", P   Q, Id, x:A. B(x), Dec(P), @i(x:T), (state when e), @i x initially v:T, @i Precondition for a:Outcome(p) is P:State(ds)   , Unit, False, R ||- es.P(es), State(ds),  es.P(es), Realizer, x(s), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rnone(), left right, Rinit(loc;T;x;v), Rpre(loc;ds;a;p;P),  |